;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Irng
  
  ; Input - A seed, integer
  ;         A max, integer
  ; Output - A pair of the new seed and a number less than max
  (sig get-random-number-mod-max (seed max))
  
  ; Input - A seed, integer
  ; Output - A new seed, integer
  (sig get-random-number (seed))
  
  ; Contract to confirm the no repeat clause
  (con rng-doesnt-repeat-values
       (implies (natp n)
                (not (equal (get-random-number n)
                            (get-random-number (get-random-number n))))))
  
)



       